package utils

import chisel3._
import chisel3.util._
import chisel3.util.experimental._
import chiseltest._

import chiseltest.formal._
import chiseltest.experimental._
import chisel3.stage.{ChiselStage, ChiselGeneratorAnnotation}

import org.scalatest.Tag
import org.scalatest.flatspec.AnyFlatSpec

import chiseltest.ChiselScalatestTester
import chiseltest.formal.backends.FormalEngineAnnotation

class FormalPipeConnSpec extends AnyFlatSpec with ChiselScalatestTester with Formal  {

  "pipeline stage" should "pass" in {
      verify(new PipeConnSpec, Seq(BoundedCheck(100), BtormcEngineAnnotation))
  }

}

class PipeConnSpec() extends Module {
    
  val port = IO(new Bundle {
    val l = Flipped(Decoupled(UInt(8.W)))
    val r = Decoupled(UInt(8.W))
    val rightOutFire = Input(Bool())
    val isFlush = Input(Bool())
  })

  PipelineConnect(port.l, port.r, port.rightOutFire, port.isFlush)

  // assert(!past(port.l.valid && port.r.ready))
  
  when(past(port.l.valid && port.r.ready)) {
    assert(port.r.bits === past(port.l.bits))
  }

}

